package typechecker.walkers;

import java.util.List;
import java.util.Vector;

import typechecker.ast.type.ForallType;
import typechecker.ast.type.FunctionType;
import typechecker.ast.type.TypeConstructorApplication;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;

/**
 * Substitutes a type variable for an type expression.
 * Before calling annot, the type expression must have 
 * every variable equal with it's binder.
 */
public class TypeSubst {
	
	private static TypeExpression substForallType(ForallType ft, TypeVariable var, TypeExpression repl){
		TypeExpression body = subst(ft.getBody(), var, repl);
		return new ForallType(ft.getQuant(), body);
	}
	
	private static TypeExpression substFunctionType(FunctionType ft, TypeVariable var, TypeExpression repl){
		TypeExpression src = subst(ft.getSrc(), var, repl);
		TypeExpression dst = subst(ft.getDest(), var, repl);
		return new FunctionType(src, dst);
	}
	
	private static TypeExpression substConstructorApplication(TypeConstructorApplication tca, TypeVariable var, TypeExpression repl){
		int size = tca.getParams().size();
		List<TypeExpression> params = new Vector<TypeExpression>(size);
		
		for(int i=0; i < size; i++){
			params.add(subst(tca.getParams().get(i), var, repl));
		}
		
		return new TypeConstructorApplication(tca.getCons(), params);
	}
	
	private static TypeExpression substVariable(TypeVariable tv, TypeVariable var, TypeExpression repl){
		if(tv.equals(var)){
			return repl;
		}else{
			return tv;
		}
	}
	
	public static TypeExpression subst(TypeExpression te, TypeVariable var, TypeExpression repl){
		if (te instanceof ForallType){
			return substForallType((ForallType)te, var, repl);
		} else if ( te instanceof FunctionType){
			return substFunctionType((FunctionType)te, var, repl);
		} else if ( te instanceof TypeConstructorApplication){
			return substConstructorApplication((TypeConstructorApplication) te, var, repl);
		} else if ( te instanceof TypeVariable){
			return substVariable((TypeVariable)te, var, repl);
		}
		return null;
	}

}
